Nuprl Lemma : leaf_value_wf
4,23
postcript
pdf
E
:Type,
t
:Tree(
E
). is_leaf(
t
)
leaf_value(
t
)
E
latex
Definitions
leaf_value(
t
)
,
Tree(
E
)
,
x
:
A
.
B
(
x
)
,
tree_con(
E
;
T
)
,
is_leaf(
t
)
,
Case tree_leaf(
x
) =>
body
(
x
)
cont
,
Case(
value
)
body
,
Default =>
body
,
{
T
}
,
b
,
True
,
P
Q
,
t
T
,
False
Lemmas
false
wf
,
true
wf
,
tree
wf
,
is
leaf
wf
,
assert
wf
origin
E:Type, t:Tree(E). is_leaf(t) 
leaf_value(t) 
E E:Type, t:Tree(E). is_leaf(t) leaf_value(t) E x:A. B(x)
b Q T